Nuprl Lemma : atom2-deq_wf
11,40
postcript
pdf
atom2-deq
EqDecider(atom{2:n})
latex
Definitions
atom2-deq
,
EqDecider(
T
)
,
atom{$n:n}
,
s
=
t
,
b
,
P
Q
,
x
:
A
B
(
x
)
,
x
:
A
.
B
(
x
)
,
<
a
,
b
>
,
t
T
,
Type
,
eq_atom{$n:n}(
x
;
y
)
,
x
.
A
(
x
)
,
atom2-deq-aux
,
prop{i:l}
,
#$n
,
,
Unit
,
left
+
right
,
,
f
(
a
)
Lemmas
iff
wf
,
assert
wf
,
atom2-deq-aux
,
eq
atom
wf2
origin
b, P 
Q, x:A
B(x), 
x:A. B(x), <a, b>, t 
T, Type, eq_atom{$n:n}(x; y), 
x.A(x), atom2-deq-aux, prop{i:l}, #$n, 
, Unit, left + right, 
, f(a)